COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	manna.lsp[w82,jmc]	ekl formalization of manna method
C00008 00003		In EKL we have the following:
C00009 ENDMK
C⊗;
manna.lsp[w82,jmc]	ekl formalization of manna method

;;; Manna method for program for multiplication by addition

	p ← 0;
	i ← n;
loop:	if i = 0 then go to done;
	i ← i - 1;
	p ← p + m;
	go to loop;
done:

We want to prove that the program reaches the symbol  done  and when
it does  p = m*n, where  *  stands for multiplication.

The Manna method involves hypothesizing that the program was faulty.
If the program were faulty, there would be a bad run for some values
of  m  and  n  that either wouldn't terminate or would terminate
with  p ≠ m*n.  Let  q(p,i)  be true for the values of  p  and  i
that are assumed during the bad run.  q  would then satisfy the
formula

q(0,n) ∧ ∀p i.q(p,i) ⊃ if i=0 then p≠m*n else q(p+m,i-1),

because if the program assumes values  p  and  i  with the program
counter at  loop  at some time during the bad run, it will either
terminate with  p ≠ m*n  or it will go around the loop to another
p  and  i  with values  p+m  and  i-1  that will again be part of
the bad run.  If we can show that the formula  (1)  is unsatisfiable,
then there can be no bad run, and we have shown that the program
terminates with the right answer.  Thus it suffices to prove

∀q m n.¬(q(0,n) ∧ ∀p i.q(p,i) ⊃ if i=0 then p≠m*n else ¬q(p+m,i-1)),

which is equivalent to the formula

∀q m n.q(0,n) ⊃ ∃p i.q(p,i) ∧ if i=0 then p=m*n else ¬q(p+m,i-1).

	We now show how this formula is easily proved working
backwards.  First we put  p = m*(n-i), i.e. we guess that this
p  will do for the  p  we must prove exists.
This leaves us trying to prove.

∀q m n.q(0,n) ⊃ ∃i.q(m*(n-i),i) ∧ if i=0 then true else ¬q(m*(n-(i-1)),i-1),

which is the same as

∀q m n.q(0,n) ⊃ ∃i.q(m*(n-i),i) ∧ (i=0 ∨ ¬q(m*(n-(i-1)),i-1).

This in turn is a special case of

∀r m n.r(n) ⊃ ∃i.r(i) ∧ (i = 0 ∨ ¬r(i-1)),

and can be obtained from it by substituting  r(i) = q(m*(n-i),i)
The latter statement can readily be proved by induction on  n.  In
fact it is just another way of expressing the schema of mathematical
induction.

	Manna's method, like inductive assertions and Hoare type
axioms, involves our inspecting the program and writing some
sentences in a logical language.  The argument that the sentences
express the desired properties of the program is metamathematical
and in practice always informal.  If we use the Elephant formalism,
however, the Manna method, and probably the others also, is just
a particular technique of using the rules of inference of logic
and the axioms of the domain to prove properties of the program.
It is merely a strategy of using certain kinds of lemmas in the
proof.

	Consider, for example, the Elephant version of the above
program.

∀t.p(t+1) = if pc(t) = 0 then 0
		else if pc(t) = 3 then p(t)+m
		else p(t)

∀t.i(t+1) = if pc(t) = 1 then n
		else if pc(t) = 4 then i(t)-1
		else i(t)

∀t.pc(t+1) =	if t=0 then 0
		else if pc(t)=2 ∧ i(t)=0 then 6
		else if pc(t)=5 then 2
		else pc(t)+1

	Our goal is to prove

∃t.pc(t)=6 ∧ p(t)=m*n

using the Elephant sentences expressing the program and the Peano axioms
of arithmetic.  Manna's method corresponds to the following proof
strategy.  Define

∀p i.q(pp,ii) ≡ [∃t.p(t)=pp ∧ i(t)=ii ∧ pc(t)=2 ∧ ∀t'.t'<t ⊃ pc(t')≠6] ∧ pp=m*(n-ii).

Using the equations of the program, we can easily prove

q(0,n)

simply by taking  t=2 and substituting.  Next we prove

∀pp ii.q(pp,ii) ⊃ if ii=0 then pp=m*n else q(pp+m,ii-1).
	In EKL we have the following:

(decl (m n p i) ground variable natnum)
(decl q |ground⊗ground → truthval|)
(decl r |ground → truthval|)

(decl psi |ground → truthval|)

(axiom |∀psi.psi(0) ∧ (∀n.psi(n) ⊃ psi(succ n)) ⊃ ∀n.psi(n)|)